\begin{tabbing}
abstract{-}chain{-}replication\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Rsp}$; ${\it isupdate}$; ${\it In}$; ${\it Out}$; ${\it Sys}$; $f$; ${\it Delta}$; $Q$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=fifo{-}antecedent(${\it es}$;${\it Sys}$;$f$)\+
\\[0ex]\& ($\forall$$u$:es{-}E{-}interface(${\it es}$;${\it Sys}$). ($f$($u$) = $u$ $\in$ es{-}E(${\it es}$)) $\Leftarrow\!\Rightarrow$ ($\uparrow$($u$ $\in_{b}$ ${\it In}$)))
\\[0ex]\& (es{-}E{-}interface(${\it es}$;${\it In}$) $\subseteq$r es{-}E{-}interface(${\it es}$;${\it Sys}$))
\\[0ex]\& (es{-}E{-}interface(${\it es}$;${\it Out}$) $\subseteq$r es{-}E{-}interface(${\it es}$;${\it Sys}$))
\\[0ex]\& ($\forall$$e$:es{-}E{-}interface(${\it es}$;${\it In}$). ($\neg$($\uparrow$(${\it isupdate}$(${\it In}$($e$))))) $\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)))
\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex]($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$))) $\Rightarrow$ (es{-}loc(${\it es}$; ($f$($e$))) = es{-}loc(${\it es}$; $e$) $\in$ Id) $\Rightarrow$ ($\neg$($\uparrow$($e$ $\in_{b}$ ${\it Out}$))))
\-\\[0ex]\& input{-}forwarding\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Sys}$; ${\it isupdate}$; ${\it In}$; $f$)
\-\\[0ex]\& ($\exists$\=${\it chain}$:es{-}E{-}interface(${\it es}$;${\it Sys}$)$\rightarrow$(Id List)\+
\\[0ex]chain{-}consistent(${\it es}$;${\it Sys}$;${\it In}$;${\it isupdate}$;${\it Out}$;$f$;${\it chain}$))
\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Out}$).\+
\\[0ex](\=is{-}query(${\it In}$;${\it isupdate}$;$e$)\+
\\[0ex]$\Rightarrow$ (${\it Out}$($e$) = $Q$(filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; $e$)),${\it In}$($e$)) $\in$ ${\it Rsp}$))
\-\\[0ex]\& (\=($\neg$is{-}query(${\it In}$;${\it isupdate}$;$e$))\+
\\[0ex]$\Rightarrow$ (${\it Out}$($e$) = ${\it Delta}$(filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; $e$))) $\in$ ${\it Rsp}$)))
\-\-\-
\end{tabbing}